f(x1) → n(c(n(a(x1))))
c(f(x1)) → f(n(a(c(x1))))
n(a(x1)) → c(x1)
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
↳ QTRS
↳ DependencyPairsProof
f(x1) → n(c(n(a(x1))))
c(f(x1)) → f(n(a(c(x1))))
n(a(x1)) → c(x1)
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
C(f(x1)) → F(n(a(c(x1))))
F(x1) → N(a(x1))
F(x1) → C(n(a(x1)))
N(f(x1)) → F(n(x1))
C(f(x1)) → C(x1)
N(a(x1)) → C(x1)
N(s(x1)) → F(s(s(x1)))
C(f(x1)) → N(a(c(x1)))
N(f(x1)) → N(x1)
F(x1) → N(c(n(a(x1))))
f(x1) → n(c(n(a(x1))))
c(f(x1)) → f(n(a(c(x1))))
n(a(x1)) → c(x1)
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
C(f(x1)) → F(n(a(c(x1))))
F(x1) → N(a(x1))
F(x1) → C(n(a(x1)))
N(f(x1)) → F(n(x1))
C(f(x1)) → C(x1)
N(a(x1)) → C(x1)
N(s(x1)) → F(s(s(x1)))
C(f(x1)) → N(a(c(x1)))
N(f(x1)) → N(x1)
F(x1) → N(c(n(a(x1))))
f(x1) → n(c(n(a(x1))))
c(f(x1)) → f(n(a(c(x1))))
n(a(x1)) → c(x1)
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
N(s(x1)) → F(s(s(x1)))
Used ordering: Polynomial interpretation [25,35]:
C(f(x1)) → F(n(a(c(x1))))
F(x1) → N(a(x1))
F(x1) → C(n(a(x1)))
N(f(x1)) → F(n(x1))
C(f(x1)) → C(x1)
N(a(x1)) → C(x1)
C(f(x1)) → N(a(c(x1)))
N(f(x1)) → N(x1)
F(x1) → N(c(n(a(x1))))
The value of delta used in the strict ordering is 1/2.
POL(C(x1)) = 0
POL(N(x1)) = (2)x_1
POL(f(x1)) = (2)x_1
POL(n(x1)) = (4)x_1
POL(c(x1)) = 0
POL(a(x1)) = 0
POL(s(x1)) = 1/4
POL(F(x1)) = 0
c(c(x1)) → c(x1)
n(f(x1)) → f(n(x1))
c(f(x1)) → f(n(a(c(x1))))
f(x1) → n(c(n(a(x1))))
n(s(x1)) → f(s(s(x1)))
n(a(x1)) → c(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(x1) → N(a(x1))
C(f(x1)) → F(n(a(c(x1))))
F(x1) → C(n(a(x1)))
C(f(x1)) → C(x1)
N(f(x1)) → F(n(x1))
N(a(x1)) → C(x1)
C(f(x1)) → N(a(c(x1)))
N(f(x1)) → N(x1)
F(x1) → N(c(n(a(x1))))
f(x1) → n(c(n(a(x1))))
c(f(x1)) → f(n(a(c(x1))))
n(a(x1)) → c(x1)
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))